AtomFreeDecls(X)
== (i, x:Id. AtomFree(Type;1of(2of(2of(2of(2of(2of(X))))))(i,x)))
== & (i:Id, k:Knd. AtomFree(Type;1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(X))))))))))(k,i))) 

latex

---

clarification:

EVal-atom-free{i:l}
EVal-atom-free(X)
== (i:Id, x:Id. AtomFree(Type{i};1of(2of(2of(2of(2of(2of(X))))))(i,x)))
== & (i:Id, k:Knd.
== & (AtomFree(Type{i};1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(X))))))))))(k,i))) 

latex

Definitions	P & Q, Id, x:A. B(x), Knd, AtomFree(T;x), Type, f(a), 1of(t), 2of(t)
FDL editor aliases	EVal-atom-free